g:OGrp, a, b:|g|. (a < b)  (e < (b * (~(a)))) 

latex

Up	groups 1
Definitions of Statement	IMonoid, Mon, IAbMonoid, AbMon, IGroup, OCMon, OGrp
Definitions	t  T, x:A. B(x), IGroup, IMonoid, IAbMonoid, True, T, P & Q, P  Q, , P  Q, x f y, P  Q, Mon, AbMon, OCMon, OGrp
Lemmas	ocgrp wf, grp car wf, inverse wf, grp inverse, comm wf, monoid p wf, abmonoid comm, grp sig wf, true wf, squash wf, iff wf, grp lt op l, grp id wf, grp inv wf, grp op wf, grp lt wf, iff functionality wrt iff